* Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) - Signature: {cons/2,f/3} / {a/0,b/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons,f} and constructors {a,b,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Weak TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) - Signature: {cons/2,f/3,cons#/2,f#/3} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#} and constructors {a,b,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) * Step 3: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Signature: {cons/2,f/3,cons#/2,f#/3} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#} and constructors {a,b,s} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:cons#(x,y) -> c_1() 2:S:cons#(x,y) -> c_2() 3:S:f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) The dependency graph contains no loops, we remove all dependency pairs. * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {cons/2,f/3,cons#/2,f#/3} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))